es:ES, e1, e2:E, P:({e:E| loc(e) = loc(e1)  Id} ).
(loc(e2) = loc(e1)  Id)  (e[e1,e2).P(e)  ) 

latex

Definitions	t  T, b, P  Q, False, A, x:A. B(x), P & Q, (e <loc e'), loc(e), Id, ES, E, , x(s), e loc e' , A c B, x:A. B(x), e[e1,e2).P(e)
Lemmas	es-le wf, es-locl wf, es-E wf, event system wf, Id wf, es-loc wf, es-le-loc, es-loc-pred